Functional Pearl: Dependent type inference via free higher-order unification